Inference at * 1 3 1 0 1 1 1 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. zz : 
  n:. (n < zz)  (P(n)) 

latex

 by InteriorProof (NatInd (-1)) 

latex

 1: .....basecase..... NILNIL

 1: 2. j:. (k:. (k < j)  (P(k)))  (P(j))
 1:   n:. (n < 0)  (P(n))
 2: .....upcase..... NILNIL

 2: 3. zz : 
 2: 4. 0 < zz
 2: 5. n:. (n < (zz - 1))  (P(n))
 2:   n:. (n < zz)  (P(n))
 .

Definitions	-n, {x:A| B(x)} , n+m, Type, Void, s = t, x:AB(x), , a < b, n - m, f(a), #$n, , , i  j , A  B, A, False, P  Q, x:A. B(x), t  T
Lemmas	nat wf, nat ind tp, ge wf, nat properties